Model Theory

I had a similar experience with model theory to that of my experience with JTB; it seems on the face of it to have principles that are neccissary for it to function formally that are seldom recognised and even less often talked about. The basic problem is this; there is a meta-theory and a subject theory. In some instances people want to talk about them being the same, they will use words like "coding" etc. To beleive the results proved in the meta about the coding of the meta we need to beleive in a principle of externalisation, this cannot be gotten from the theory. If youre a platonist this might not be a problem for you I suppose (Godel was), the languages are talking about the same platonic objects. Well I found some discussions on the matter that I just want to collect here for my own sanity:

• https://cs.nyu.edu/pipermail/fom/2020-January/021874.html : An email between Timothy Chow and Detlefsen discussion the extra unspoken principle (in the context of Godels theorem)
• Hilbert's Program: An Essay on Mathematical Instrumentalism, vol. 182 of the Synthese Library, D. Reidel Publishing Co.,1986, ISBN 978-94-015-7731-1 : Detlefsen's book on the problem, and how it effects the commonly touted defeat of Hilberts program
• https://math.stackexchange.com/q/4835354/1273463 : A pretty confused post I made on the matter.
• https://math.stackexchange.com/a/4360940/1273463 : Points out that the meta-theory can be much weaker than the subject theory.

• https://math.stackexchange.com/a/3574484/1273463 : A good defense of the "forget about foundations" approach given by Kruckman, the best statement is in the comments

  "Mathematics is a social enterprise, which is carried out in natural language. Vanishingly few theorems have actually been formalized in ZFC. Now to make mathematics a coherent enterprise, we have to agree on what counts as a proof, and the common consensus is we accept a proof if it can in principle be formalized in ZFC. Those who care put in the work to carefully understand what can be formalized but the majority just pick up the intuition for this as they get socialized into the mathematical community."

  is true but not helpful if you happen to be one of the people who want to put in the work.

• https://mathoverflow.net/q/22635/519939 : A better articulation of my question. The answers by Timothy Chow and Peter LeFanu Lumsdaine are fantastic.
• https://mathoverflow.net/q/248965/519939 : Is a very interesting discussion with the most relevant answers being by Burak
• Kunen writes "The metatheory consists of what is really true." (1980, p.7, his emphasis) as part of a longer explanation. Try to figure out what axiomatic theory that is! His goal is to avoid having to pin himself down - he wants the reader to be able to insert their own metatheory on top of his exposition.
• https://mathoverflow.net/q/437195 : Some interesting discussions in the comments